/-
Copyright (c) 2021 Chris Hughes. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Chris Hughes
-/
import Mathlib.Algebra.MvPolynomial.CommRing

/-!
# Algebraic Independence

This file defines algebraic independence of a family of elements of an `R` algebra.

## Main definitions

* `AlgebraicIndependent` - `AlgebraicIndependent R x` states the family of elements `x`
  is algebraically independent over `R`, meaning that the canonical map out of the multivariable
  polynomial ring is injective.

* `AlgebraicIndependent.aevalEquiv` - The canonical isomorphism from the polynomial ring to the
  subalgebra generated by an algebraic independent family.

* `AlgebraicIndependent.repr` - The canonical map from the subalgebra generated by an
  algebraic independent family into the polynomial ring. It is the inverse of
  `AlgebraicIndependent.aevalEquiv`.

* `IsTranscendenceBasis R x` - a family `x` is a transcendence basis over `R` if it is a maximal
  algebraically independent subset.

## Main results

We show that algebraic independence is preserved under injective maps of the indices.

## References

* [Stacks: Transcendence](https://stacks.math.columbia.edu/tag/030D)

-/


noncomputable section

open Function Set Subalgebra MvPolynomial Algebra

variable {ι ι' : Type*} (R : Type*) {K A A' : Type*} (x : ι → A)
variable [CommRing R] [CommRing A] [CommRing A'] [Algebra R A] [Algebra R A']

/-- `AlgebraicIndependent R x` states the family of elements `x`
  is algebraically independent over `R`, meaning that the canonical
  map out of the multivariable polynomial ring is injective. -/
@[stacks 030E "(1)"] def AlgebraicIndependent : Prop :=
  Injective (MvPolynomial.aeval x : MvPolynomial ι R →ₐ[R] A)

/-- `AlgebraicIndepOn R v s` states that the elements in the family `v` that are indexed by the
elements of `s` are algebraically independent over `R`. -/
abbrev AlgebraicIndepOn (s : Set ι) : Prop := AlgebraicIndependent R fun i : s ↦ x i

variable {R} {x}

theorem algebraicIndependent_iff :
    AlgebraicIndependent R x ↔
      ∀ p : MvPolynomial ι R, MvPolynomial.aeval (x : ι → A) p = 0 → p = 0 :=
  injective_iff_map_eq_zero _

theorem AlgebraicIndependent.eq_zero_of_aeval_eq_zero (h : AlgebraicIndependent R x) :
    ∀ p : MvPolynomial ι R, MvPolynomial.aeval (x : ι → A) p = 0 → p = 0 :=
  algebraicIndependent_iff.1 h

theorem algebraicIndependent_iff_injective_aeval :
    AlgebraicIndependent R x ↔ Injective (MvPolynomial.aeval x : MvPolynomial ι R →ₐ[R] A) :=
  Iff.rfl

namespace AlgebraicIndependent

theorem of_comp (f : A →ₐ[R] A') (hfv : AlgebraicIndependent R (f ∘ x)) :
    AlgebraicIndependent R x := by
  have : aeval (f ∘ x) = f.comp (aeval x) := by ext; simp
  rw [AlgebraicIndependent, this, AlgHom.coe_comp] at hfv
  exact hfv.of_comp

variable (hx : AlgebraicIndependent R x)
include hx

theorem comp (f : ι' → ι) (hf : Function.Injective f) : AlgebraicIndependent R (x ∘ f) := by
  intro p q
  simpa [aeval_rename, (rename_injective f hf).eq_iff] using @hx (rename f p) (rename f q)

theorem coe_range : AlgebraicIndependent R ((↑) : range x → A) := by
  simpa using hx.comp _ (rangeSplitting_injective x)

end AlgebraicIndependent

open AlgebraicIndependent

theorem algebraicIndependent_equiv (e : ι ≃ ι') {f : ι' → A} :
    AlgebraicIndependent R (f ∘ e) ↔ AlgebraicIndependent R f :=
  ⟨fun h => Function.comp_id f ▸ e.self_comp_symm ▸ h.comp _ e.symm.injective,
    fun h => h.comp _ e.injective⟩

theorem algebraicIndependent_equiv' (e : ι ≃ ι') {f : ι' → A} {g : ι → A} (h : f ∘ e = g) :
    AlgebraicIndependent R g ↔ AlgebraicIndependent R f :=
  h ▸ algebraicIndependent_equiv e

theorem algebraicIndependent_subtype_range {ι} {f : ι → A} (hf : Injective f) :
    AlgebraicIndependent R ((↑) : range f → A) ↔ AlgebraicIndependent R f :=
  Iff.symm <| algebraicIndependent_equiv' (Equiv.ofInjective f hf) rfl

alias ⟨AlgebraicIndependent.of_subtype_range, _⟩ := algebraicIndependent_subtype_range

theorem algebraicIndependent_image {ι} {s : Set ι} {f : ι → A} (hf : Set.InjOn f s) :
    (AlgebraicIndependent R fun x : s => f x) ↔ AlgebraicIndependent R fun x : f '' s => (x : A) :=
  algebraicIndependent_equiv' (Equiv.Set.imageOfInjOn _ _ hf) rfl

namespace AlgebraicIndependent

theorem mono {t s : Set A} (h : t ⊆ s)
    (hx : AlgebraicIndependent R ((↑) : s → A)) : AlgebraicIndependent R ((↑) : t → A) := by
  simpa [Function.comp] using hx.comp (inclusion h) (inclusion_injective h)

section repr

variable (hx : AlgebraicIndependent R x)
include hx

/-- Canonical isomorphism between polynomials and the subalgebra generated by
  algebraically independent elements. -/
@[simps! apply_coe]
def aevalEquiv : MvPolynomial ι R ≃ₐ[R] Algebra.adjoin R (range x) :=
  (AlgEquiv.ofInjective (aeval x) (algebraicIndependent_iff_injective_aeval.1 hx)).trans
    (Subalgebra.equivOfEq _ _ (Algebra.adjoin_range_eq_range_aeval R x).symm)

@[simp]
theorem algebraMap_aevalEquiv (p : MvPolynomial ι R) :
    algebraMap (Algebra.adjoin R (range x)) A (hx.aevalEquiv p) = aeval x p :=
  rfl

/-- The canonical map from the subalgebra generated by an algebraic independent family
  into the polynomial ring. -/
def repr : Algebra.adjoin R (range x) →ₐ[R] MvPolynomial ι R :=
  hx.aevalEquiv.symm

@[simp]
theorem aeval_repr (p) : aeval x (hx.repr p) = p :=
  Subtype.ext_iff.1 (AlgEquiv.apply_symm_apply hx.aevalEquiv p)

theorem aeval_comp_repr : (aeval x).comp hx.repr = Subalgebra.val _ :=
  AlgHom.ext hx.aeval_repr

end repr

end AlgebraicIndependent

variable (R) in
/-- A family is a transcendence basis if it is a maximal algebraically independent subset. -/
@[stacks 030E "(4)"] def IsTranscendenceBasis (x : ι → A) : Prop :=
  AlgebraicIndependent R x ∧
    ∀ (s : Set A) (_ : AlgebraicIndepOn R id s) (_ : range x ⊆ s), range x = s

theorem isTranscendenceBasis_iff_maximal {s : Set A} :
    IsTranscendenceBasis R ((↑) : s → A) ↔ Maximal (AlgebraicIndepOn R id) s := by
  rw [IsTranscendenceBasis, maximal_iff, Subtype.range_val]; rfl

theorem isTranscendenceBasis_equiv (e : ι ≃ ι') {f : ι' → A} :
    IsTranscendenceBasis R (f ∘ e) ↔ IsTranscendenceBasis R f := by
  simp_rw [IsTranscendenceBasis, algebraicIndependent_equiv, EquivLike.range_comp]

alias ⟨_, IsTranscendenceBasis.comp_equiv⟩ := isTranscendenceBasis_equiv

theorem isTranscendenceBasis_equiv' (e : ι ≃ ι') {f : ι' → A} {g : ι → A} (h : f ∘ e = g) :
    IsTranscendenceBasis R g ↔ IsTranscendenceBasis R f :=
  h ▸ isTranscendenceBasis_equiv e

theorem isTranscendenceBasis_subtype_range {ι} {f : ι → A} (hf : Injective f) :
    IsTranscendenceBasis R ((↑) : range f → A) ↔ IsTranscendenceBasis R f :=
  .symm <| isTranscendenceBasis_equiv' (Equiv.ofInjective f hf) rfl

alias ⟨IsTranscendenceBasis.of_subtype_range, _⟩ := isTranscendenceBasis_subtype_range

theorem isTranscendenceBasis_image {ι} {s : Set ι} {f : ι → A} (hf : Set.InjOn f s) :
    IsTranscendenceBasis R (fun x : s ↦ f x) ↔ IsTranscendenceBasis R fun x : f '' s ↦ (x : A) :=
  isTranscendenceBasis_equiv' (Equiv.Set.imageOfInjOn _ _ hf) rfl
